T:Type, R:(TT).
Trans(T;x,y.R(x,y))
 {a, a', b, b':T.
 Symmetrize(x,y.R(x,y);a;b)  Symmetrize(x,y.R(x,y);a';b')  (R(a,a')  R(b,b'))} 

latex

ProofTree

Definitions	x,y. t(x;y), t  T, P  Q, P & Q, P  Q, Symmetrize(x,y.R(x;y);a;b), {T}, x(s1,s2), P  Q, , x:A. B(x)
Lemmas	trans wf, trans rel self functionality